/**
 * Copyright (c) 2010 by Kevin Bierhoff.
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *    1. Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *    2. Redistributions in binary form must reproduce the above copyright
 *       notice, this list of conditions and the following disclaimer in the
 *       documentation and/or other materials provided with the distribution.
 *    3. Neither the names of the authors nor the
 *       names of its contributors may be used to endorse or promote products
 *       derived from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE AUTHORS ''AS IS'' AND ANY
 * EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
 * WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY
 * DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
 * INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
 * LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
 * ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
 * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 */
package com.googlecode.syper.javasyp.checker;

import java.util.Collections;
import java.util.List;

import org.eclipse.jdt.core.dom.ASTVisitor;
import org.eclipse.jdt.core.dom.ArrayAccess;
import org.eclipse.jdt.core.dom.ArrayCreation;
import org.eclipse.jdt.core.dom.ArrayInitializer;
import org.eclipse.jdt.core.dom.Assignment;
import org.eclipse.jdt.core.dom.BodyDeclaration;
import org.eclipse.jdt.core.dom.BooleanLiteral;
import org.eclipse.jdt.core.dom.CastExpression;
import org.eclipse.jdt.core.dom.CharacterLiteral;
import org.eclipse.jdt.core.dom.ClassInstanceCreation;
import org.eclipse.jdt.core.dom.ConditionalExpression;
import org.eclipse.jdt.core.dom.Expression;
import org.eclipse.jdt.core.dom.FieldAccess;
import org.eclipse.jdt.core.dom.ITypeBinding;
import org.eclipse.jdt.core.dom.IVariableBinding;
import org.eclipse.jdt.core.dom.InfixExpression;
import org.eclipse.jdt.core.dom.InstanceofExpression;
import org.eclipse.jdt.core.dom.MethodDeclaration;
import org.eclipse.jdt.core.dom.MethodInvocation;
import org.eclipse.jdt.core.dom.Modifier;
import org.eclipse.jdt.core.dom.NullLiteral;
import org.eclipse.jdt.core.dom.NumberLiteral;
import org.eclipse.jdt.core.dom.ParenthesizedExpression;
import org.eclipse.jdt.core.dom.PostfixExpression;
import org.eclipse.jdt.core.dom.PrefixExpression;
import org.eclipse.jdt.core.dom.QualifiedName;
import org.eclipse.jdt.core.dom.SimpleName;
import org.eclipse.jdt.core.dom.SingleVariableDeclaration;
import org.eclipse.jdt.core.dom.StringLiteral;
import org.eclipse.jdt.core.dom.SuperFieldAccess;
import org.eclipse.jdt.core.dom.SuperMethodInvocation;
import org.eclipse.jdt.core.dom.ThisExpression;
import org.eclipse.jdt.core.dom.TypeLiteral;
import org.eclipse.jdt.core.dom.VariableDeclarationExpression;
import org.eclipse.jdt.core.dom.InfixExpression.Operator;

import com.googlecode.syper.anno.Pred;
import com.googlecode.syper.javasyp.formulae.Field;
import com.googlecode.syper.javasyp.formulae.Formula;
import com.googlecode.syper.javasyp.formulae.IfThenElse;
import com.googlecode.syper.javasyp.formulae.Infix;
import com.googlecode.syper.javasyp.formulae.Literal;
import com.googlecode.syper.javasyp.formulae.Local;
import com.googlecode.syper.javasyp.formulae.Pre;
import com.googlecode.syper.javasyp.formulae.Prefix;
import com.googlecode.syper.javasyp.formulae.Quantifier;
import com.googlecode.syper.javasyp.formulae.Ref;

/**
 * @author kevin
 * @since Jan 30, 2010
 */
public class ExpressionEncoder extends ASTVisitor {

	interface Lookup {

		/**
		 * Returns a reference representing the given expression.
		 * This can be a {@link Local} or {@link Pre}.
		 * @param e must not refer to a field
		 * @return a reference representing the given expression
		 */
		Ref getName(Expression e);

		/**
		 * Returns a field reference for the given accessor ref and field
		 * @param accessor An object reference
		 * @param field Field binding (not static or enum) or {@code null} for array.length "field"
		 * @return a field reference for the given accessor ref and field
		 */
		Field getField(Ref accessor, IVariableBinding field);

		/**
		 * Returns a array select for the given array and index
		 * @param array
		 * @param index
		 * @param elementType type of the selected array element
		 * @return a array select for the given array and index
		 */
		Ref getSelect(Formula array, Formula index, ITypeBinding elementType);
	}

	/**
	 * Encodes the given expression as a formula using the given lookup callback
	 * @param e
	 * @param lookup
	 * @return the given expression as a formula
	 */
	public static Formula encode(Expression e, Lookup lookup) {
		return encode(e, lookup, false);
	}

	/**
	 * Encodes the given expression as a formula using the given lookup callback
	 * @param e
	 * @param lookup
	 * @param standalone indicates if the expression is to be encoded
	 * as one formula, no temps
	 * @return the given expression as a formula
	 */
	static Formula encode(Expression e, Lookup lookup, boolean standalone) {
		ExpressionEncoder enc = new ExpressionEncoder(lookup, standalone);
		return encode(enc, e);
	}

	/** only for subclasses */
	protected static Formula encode(ExpressionEncoder enc, Expression e) {
		e.accept(enc);
		if (enc.result == null)
			throw new NullPointerException("no encoding: " + e);
		return enc.result;
	}

	private Formula result;
	private final Lookup lookup;
	private final boolean standalone;

	public ExpressionEncoder(Lookup lookup, boolean standalone) {
		this.lookup = lookup;
		this.standalone = standalone;
	}

	/**
	 * Helper to call {@link #encode(Expression, Lookup, boolean)} recursively
	 * @param expression
	 * @return
	 */
	protected final Formula encodeChild(Expression e) {
		return encodeChild(e, standalone);
	}

	/**
	 * Helper to call {@link #encode(Expression, Lookup, boolean)} recursively
	 * @param expression
	 * @return
	 */
	protected final Formula encodeChild(Expression e, boolean newStandalone) {
		ExpressionEncoder childEncoder = newInstance(lookup, newStandalone);
		return encode(childEncoder, e);
//		return encode(e, lookup, newStandalone);
	}

	/**
	 * Indicates if the expression is to be encoded in one formula, no temps
	 * @return
	 */
	protected final boolean isStandalone() {
		return standalone;
	}

	protected final void setResult(Formula result) {
		this.result = result;
	}

	protected ExpressionEncoder newInstance(Lookup newLookup, boolean newStandalone) {
		return new ExpressionEncoder(newLookup, newStandalone);
	}

	@Override
	public boolean visit(ArrayAccess node) {
		Formula array = encodeChild(node.getArray());
		Formula index = encodeChild(node.getIndex());
		result = lookup.getSelect(array, index, node.resolveTypeBinding());
		return false;
	}

	@Override
	public boolean visit(ArrayCreation node) {
		result = lookup.getName(node);
		return false;
	}

	@Override
	public boolean visit(ArrayInitializer node) {
		result = lookup.getName(node);
		return false;
	}

	@Override
	public boolean visit(Assignment node) {
		if (Assignment.Operator.ASSIGN == node.getOperator())
			node.getRightHandSide().accept(this);
		else
			result = lookup.getName(node);
		return false;
	}

	@Override
	public void endVisit(BooleanLiteral node) {
		result = Literal.getLiteral(node);
	}

	@Override
	public void endVisit(CastExpression node) {
		// result contains node.getExpression()'s encoding
	}

	@Override
	public void endVisit(CharacterLiteral node) {
		result = Literal.getLiteral(node);
	}

	@Override
	public boolean visit(ClassInstanceCreation node) {
		result = lookup.getName(node);
		return false;
	}

	@Override
	public boolean visit(ConditionalExpression node) {
		if (isStandalone()) {
			Formula cond = encodeChild(node.getExpression());
			Formula thenF = encodeChild(node.getThenExpression());
			Formula elseF = encodeChild(node.getElseExpression());
			result = new IfThenElse(cond, thenF, elseF);
		} else {
			result = lookup.getName(node);
		}
		return false;
	}

	@Override
	public boolean visit(FieldAccess node) {
		Ref access = (Ref) encodeChild(node.getExpression());
		result = lookup.getField(access, node.resolveFieldBinding());
		return false;
	}

	@Override
	@SuppressWarnings("unchecked")
	public boolean visit(InfixExpression node) {
		Formula lhs = encodeChild(node.getLeftOperand());
		Formula rhs = encodeChild(node.getRightOperand());
		lhs = new Infix(lhs, node.getOperator(), rhs);
		for (Expression e : (List<Expression>) node.extendedOperands()) {
			rhs = encodeChild(e);
			lhs = new Infix(lhs, node.getOperator(), rhs);
		}
		result = lhs;
		return false;
	}

	@Override
	public void endVisit(InstanceofExpression node) {
		throw new UnsupportedOperationException("cannot encode " + node);
	}

	@Override
	@SuppressWarnings("unchecked")
	public boolean visit(MethodInvocation node) {
		String mname = node.getName().getIdentifier();
		if (("forall".equals(mname) || "exists".equals(mname)) &&
				Modifier.isStatic(node.resolveMethodBinding().getModifiers()) &&
				Pred.class.getName().equals(node.resolveMethodBinding().getDeclaringClass().getQualifiedName())) {
			Formula start = encodeChild((Expression) node.arguments().get(0));
			Formula end = encodeChild((Expression) node.arguments().get(1));
			ClassInstanceCreation body = (ClassInstanceCreation) node.arguments().get(2);
			for (BodyDeclaration b : (List<BodyDeclaration>) body.getAnonymousClassDeclaration().bodyDeclarations()) {
				if (b instanceof MethodDeclaration) {
					MethodDeclaration m = (MethodDeclaration) b;
					if ("cond".equals(m.getName().getIdentifier())) {
						Expression cond = ReturnFinder.findReturn(m).getExpression();
						Formula pred = encodeChild(cond, true /* anonymous inner class expression never available as temp */);
						Local i = new Local(((SingleVariableDeclaration) m.parameters().get(0)).getName().getIdentifier(),
								node.getAST().resolveWellKnownType("int"));
						if ("forall".equals(mname)) {
							// forall i . [in-range] ==> pred
							result = Quantifier.forall(
								Collections.singletonList(i),
								Infix.toInfix(Operator.OR,
									Prefix.not(Infix.toInfix(Operator.AND,
										Infix.toInfix(Operator.LESS_EQUALS, start, i),
										Infix.toInfix(Operator.LESS, i, end))),
									pred));
						} else if ("exists".equals(mname)) {
							// exists i . [in-range] & pred
							result = Quantifier.exists(
									Collections.singletonList(i),
									Infix.toInfix(Operator.AND,
										Infix.toInfix(Operator.LESS_EQUALS, start, i),
										Infix.toInfix(Operator.LESS, i, end),
										pred));
						} else {
							throw new IllegalStateException("I thought we checked: " + mname);
						}
					}
				}
			}
			return false;
		}

		result = lookup.getName(node);
		return false;
	}

	@Override
	public void endVisit(NullLiteral node) {
		result = Literal.NULL;
		super.endVisit(node);
	}

	@Override
	public void endVisit(NumberLiteral node) {
		result = Literal.getLiteral(node);
		super.endVisit(node);
	}

	@Override
	public void endVisit(ParenthesizedExpression node) {
		// nothing: result contains translation of node.getExpression()
		super.endVisit(node);
	}

	@Override
	public boolean visit(PostfixExpression node) {
		result = lookup.getName(node);
		return false;
	}

	@Override
	public boolean visit(PrefixExpression node) {
		if (AssignedFinder.ASSIGNING_PREPOST_OPS.contains(node.getOperator())) {
			result = lookup.getName(node);
		} else {
			result = new Prefix(node.getOperator(), encodeChild(node.getOperand()));
		}
		return false;
	}

	@Override
	public boolean visit(QualifiedName node) {
		if (node.resolveBinding() instanceof IVariableBinding) {
			IVariableBinding field = (IVariableBinding) node.resolveBinding();
			Ref access = (Ref) encodeChild(node.getQualifier());
			result = lookup.getField(access, field);
			return false;
		}
		throw new UnsupportedOperationException("cannot encode " + node);
	}

	@Override
	public void endVisit(SimpleName node) {
		result = lookup.getName(node);
//		if (node.resolveBinding() instanceof IVariableBinding) {
//			IVariableBinding binding = (IVariableBinding) node.resolveBinding();
//			if (binding.isField()) {
//				if (Modifier.isStatic(binding.getModifiers()))
//					throw new UnsupportedOperationException("cannot encode " + node);
//				result = lookup.getField(null, binding);
//			} else { // local
//				result = lookup.getName(node);
//			}
//		}
	}

	@Override
	public void endVisit(StringLiteral node) {
		result = Literal.getLiteral(node);
		super.endVisit(node);
	}

	@Override
	public void endVisit(SuperFieldAccess node) {
		throw new UnsupportedOperationException("cannot encode " + node);
	}

	@Override
	public void endVisit(SuperMethodInvocation node) {
		throw new UnsupportedOperationException("cannot encode " + node);
	}

	@Override
	public void endVisit(ThisExpression node) {
		result = lookup.getName(node);
	}

	@Override
	public void endVisit(TypeLiteral node) {
		result = Literal.getLiteral(node);
	}

	@Override
	public void endVisit(VariableDeclarationExpression node) {
		throw new UnsupportedOperationException("cannot encode " + node);
	}

}
